$\forall$$l$:IdLnk, ${\it dt}$:${\it tg}$:Id fp$\rightarrow$ Type, ${\it knd}$:Knd, $T$:Type. \\[0ex](isrcv(${\it knd}$) $\Rightarrow$ lnk(${\it knd}$) $=$ $l$ $\Rightarrow$ $T$ $=$ ${\it dt}$(tag(${\it knd}$))?Void) $\Rightarrow$ lnk{-}decl($l$;${\it dt}$) $\parallel$ ${\it knd}$ : $T$